A, B:Type, opa:(AAA), opb:(BBB), f:(AB).
Inj(A;B;f)  FunThru2op(A;B;opa;opb;f)  Assoc(B;opb)  Assoc(A;opa) 

latex

Up	gen algebra 1
Definitions of Statement	Assoc(T;op), FunThru2op(A;B;opa;opb;f)
Definitions	t  T, Assoc(T;op), P  Q, x:A. B(x), P & Q, P  Q, P  Q, x f y, FunThru2op(A;B;opa;opb;f), Inj(A;B;f),
Lemmas	inject wf, fun thru 2op wf, assoc wf